package ch.epfl.lara.matcheck.util.printer;

import ch.epfl.lara.matcheck.ast.Formula

object PrettyStringerFormula extends FormatterTrees[Formula] {
 
  import ch.epfl.lara.matcheck.ast._
  
  def apply(formula: Formula) = format(formula) 
  
  override protected def format(formula: Formula): String = formula  match {
    case And(left,right) => "(" + format(left) + " & " + NL + format(right) + ")"
    case Or(left,right) => "(" + format(left) + " | " + NL + format(right) + ")"
    case Imply(left,right) => format(Or(Neg(left),right))
    case Neg(f) => "~(" + format(f) + ")"
    case Equality(e,f) => "(" + format(e) + " = " + format(f) + ")"
    case SetComprehension(x,f) => "{" + x + ". " + format(f) + "}"
    case SubsetEq(left,right) => "(" + format(left) + ")" + " \\subseteq " + "(" + format(right) + ")"
    case EqSet(left,right) => "(" + format(left) + ")" +  " = " + "(" + format(right) + ")"
    case In(x,set) => format(x) + " \\in " + format(set) 
    case Forall(x,f) => "\\forall " + x + "." + "(" + format(f) + ")" 
    case Tru => "true"
    case Flse => "false"
    case Function(name,elems) => name + elems.map(format(_)).mkString("(",",",")")
    case Deref(obj,field) => format(obj) + "." + format(field) 
    case Element(name) => name
    case StringLit0(string) => "\"" + string + "\""
    case Set(name) => name
    case EmptySet => "empty"
    case Union(left,right) => format(left) + " \\Un " + format(right)
    case Intersection(left,right) => format(left) + " \\Int " + format(right)
    case Eq(left,right) => "(" + format(left) + ")" +  " == " + "(" + format(right) + ")"
    case NotEq(left,right) => format(Neg(Eq(left,right)))
    case Less(left,right) => "(" + format(left) + ")" + " < " + "(" + format(right) + ")"
    case LessEq(left,right) => "(" + format(left) + ")" + " <= " + "(" + format(right) + ")"
    case Const(n) => n + ""
    case Plus(left,right)  => "(" + format(left) + " + " + format(right) + ")"
    case Minus(left,right) => "(" + format(left) + " - " + format(right) + ")"
    case Prod(left,right)  => "(" + format(left) + " * " + format(right) + ")"
    case Div(left,right)   => "(" + format(left) + " / " + format(right) + ")"
    case Mod(left,right)   => "(" + format(left) + " % " + format(right) + ")"
    // Internal cases   
    //case Equality(left,right) => "(" + format(left) + ")" +  " = " + "(" + format(right) + ")"
    case IntVar(x) => x
  }

}
